T:Type, f:(TT), x, y, z:T. y is f*(x)  z is f*(y)  z is f*(x) 

latex

Definitions	y is f*(x), P  Q, Type, y=f*(x) via L, type List, x:A. B(x), x:AB(x), x:A. B(x), x:A  B(x), hd(l), last(L), {i..j}, -n, f(a), A, l[i], n+m, #$n, [], P & Q, s = t, a < b, False, Void, b, as @ bs, [car / cdr], A List, , P  Q, P  Q, {T}, t  T, T, True
Lemmas	true wf, squash wf, fun-path-append, append wf, assert wf, last lemma, fun-path wf